(declare-sort S0 0)

(declare-sort S1 0)

(declare-const i0 Int)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i8 Int)
(declare-const i10 Int)
(push)
(declare-const i17 Int)
(declare-const i19 Int)
(declare-const i20 Int)
(declare-const i22 Int)
(declare-const i23 Int)
(declare-const i24 Int)
(assert (or (<= (mod (abs (+ 77 i3 77)) (+ 641 76 (div i2 i8) i3)) i17)))
(assert (or (= (abs (+ 77 i3 77)) (div (+ 77 i3 77) (div (- i2) 68)) i4 (+ 77 i3 77))))
(check-sat)
